g:IMonoid, b:. IsMonHom{g,g}(p:|g|. when b. p) 

latex

Up	groups 1
Definitions of Statement	IMonoid, IsMonHom{M1,M2}(f)
Definitions	t  T, FunThru2op(A;B;opa;opb;f), P & Q, x:T. b(x), IsMonHom{M1,M2}(f), x:A. B(x), IMonoid
Lemmas	imon wf, bool wf, mon when of id, grp car wf, mon when thru op